PR summary a0706e7100

Import changes for modified files

No significant changes to the import graph

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit a0706e7).

• +0 new declarations
• −0 removed declarations

No declaration differences.

No changes to strong technical debt.

No changes to weak technical debt.

Current commit a0706e7100
Reference commit c368140668

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

!radar

Benchmark results for a0706e7 against c368140 are in. No significant results found. @SnirBroshi

• ✅ build//instructions: -224.4G (-0.14%)

Small changes (1✅)

1 hidden